{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses,
  FlexibleInstances, UndecidableInstances, TemplateHaskell, QuasiQuotes #-}

{-# OPTIONS_GHC -fcontext-stack=200 #-}

{- |

Module      :  Examples.LL
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Lambda lifting yoko example.

-}
module Examples.LL where

import qualified Examples.InnerBase as I

import qualified Data.Set as Set
import qualified Data.IntMap as IM

import Examples.LLBasics

import qualified Examples.InnerGeneric as IG
import qualified Examples.LLGeneric ()

import Data.Yoko





lambdaLift :: Inner -> [Type] -> Prog
lambdaLift x e = Prog ds tm where (tm, ds) = runMnd (ll x) (e, IM.empty, 0)

llLam (IG.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where
  updE (rho, rn) = (ty : rho, support `prepend` rn) where
    support =
      IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm
llVar (IG.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i

---------------------------------------- default
ll :: Inner -> Mnd Term; ll = applyA $ LL `atM2` [qP|IdM|]

data LL m t = LL; wraps_trivially ''LL

type instance t ::? DomainA (LL IdM) = t ::? (:=:) Inner
type instance Dom (LL m) t = t
type instance Rng (LL m) t = TApp (LL m) t
type instance Idiom (LL m) = Mnd
type instance TApp (LL m) Inner = Term

instance (IdM ~ m) => Inner ::: DomainA (LL m) where
  membership = AppABy $ \ ~LL -> dcDispatch $
    weakenOrNT (llLam .|. llVar) $ NT $ imageAInDTU LL
      




env0 = [TBool, TBool, TInt `TArrow` TInt `TArrow` TInt, TInt]
ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0
ex1 = ex0 `I.App` I.Var 3
ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`
      (I.Lam TInt $ I.Var 0)

-- *LL> lambdaLift ex1 env0
--Prog [([TArrow TInt (TArrow TInt TInt),TInt],TInt,App (App (Var 2) (Var 1)) (Var 0)),
--      ([TArrow TInt (TArrow TInt TInt)],TInt,App (App (DVar 0) (Var 1)) (Var 0))
--     ] (App (App (DVar 0) (Var 2)) (Var 3))
